﻿using System.Diagnostics.Contracts;
using CodePlex.Diagnostics.Contracts.Conditions;

namespace CodePlex.Diagnostics.Contracts
{
  [ContractClassFor(typeof(IInitializable))]
  public class IInitializableContract : IInitializable
  {
    #region IInitializable Members

    void IInitializable.Initialize(bool validate)
    {
      Contract.Ensures(!((IInitializable)this).IsInitialized || !validate || this.IsValid());

      // Invariants using IsInitialized will automatically kick-in when IsInitialized is true.
    }

    bool IInitializable.IsInitialized
    {
      get
      {
        // This ensures is omitted for performance reasons:
        // we don't want IsValid to be called for every get of IsInitialized.
        // Contract.Ensures(!Contract.Result<bool>() || this.IsValid());
        return default(bool);
      }
      set
      {
        Contract.Ensures(((IInitializable)this).IsInitialized == value);
        Contract.Ensures(!((IInitializable)this).IsInitialized || this.IsValid());

        // Invariants using IsInitialized will automatically kick-in when value is true.
      }
    }

    #endregion
  }
}
